-module(prop_basics).
-include_lib("proper/include/proper.hrl").
-include("../src/rtps.hrl").
-include("../src/rtps_history_cache.hrl").

-export([items/0]).


%%%%%%%%%%%%%%%%%%
%%% Properties %%%
%%%%%%%%%%%%%%%%%%
prop_add_domain() ->
    ?SETUP(fun() -> 
		   application:start(rtps),
		   fun() -> application:stop(rtps) end
	   end,
	   ?FORALL(Domain_id, rtps:domain_id(),
		   begin
		       case rtps:add_domain(Domain_id) of
			   {ok, _Pid} ->
			       true;
			   {error, {already_started, _Pid}} ->
			       true;
			   _ ->
			       false
		       end
		   end)
	).

prop_del_domain() ->
    ?SETUP(fun() -> 
		   application:start(rtps),
		   fun() -> application:stop(rtps) end
	   end,
	   ?FORALL(Domain_id, rtps:domain_id(),
		   begin
		       {ok, _Pid} = rtps:add_domain(Domain_id),
		       Domain_pid = rtps:whereis(Domain_id),
		       true = is_pid(Domain_pid),
		       rtps:del_domain(Domain_id),
		       undefined =:= rtps:whereis(Domain_id)
		   end)
	).

prop_add_participant() ->
    Domain_id = 0,
    ?SETUP(fun() -> 
		   application:start(rtps),
		   rtps:add_domain(Domain_id),
		   fun() -> application:stop(rtps) end
	   end,
	   ?FORALL(Guid_prefix, ?SUCHTHAT(G, rtps:guid_prefix(), G =/= unknown),
		   begin
		       case rtps:add_participant(Domain_id, Guid_prefix) of
			   {ok, _Pid} ->
			       true;
			   {error, {already_started, _Pid}} ->
			       true;
			   _ ->
			       false
		       end
		   end)
	  ).

prop_del_participant() ->
    Domain_id = 0,
    ?SETUP(fun() -> 
		   application:start(rtps),
		   rtps:add_domain(Domain_id),
		   fun() -> application:stop(rtps) end
	   end,
	   ?FORALL(Guid_prefix, ?SUCHTHAT(G, rtps:guid_prefix(), G =/= unknown),
		   begin
		       {ok, _Pid} = rtps:add_participant(Domain_id, Guid_prefix),
		       Participant_pid = rtps:whereis(Domain_id, Guid_prefix),
		       true = is_pid(Participant_pid),
		       rtps:del_participant(Domain_id, Guid_prefix),
		       undefined =:= rtps:whereis(Domain_id, Guid_prefix)
		   end)
	).

prop_add_writer() ->
    Domain_id = 0,
    Guid_prefix = <<1:96>>,
    ?SETUP(fun() -> 
		   application:start(rtps),
		   rtps:add_domain(Domain_id),
		   rtps:add_participant(Domain_id, Guid_prefix),
		   fun() -> application:stop(rtps) end
	   end,
	   ?FORALL({Entity_key,
		    State_type,
		    Reliability_level}, {rtps:entity_key(),
					 oneof([stateless, stateful]),
					 oneof([best_effort, reliable])},
		   begin
		       Opts = [{state_type, State_type}, {reliability_level, Reliability_level}],
		       case rtps:add_writer(Domain_id, Guid_prefix, Entity_key, Opts) of
			   {ok, _Pid} ->
			       true;
			   {error, {already_started, _Pid}} ->
			       true;
			   _ ->
			       false
		       end
		   end)
	  ).

prop_del_writer() ->
    Domain_id = 0,
    Guid_prefix = <<1:96>>,
    ?SETUP(fun() -> 
		   application:start(rtps),
		   rtps:add_domain(Domain_id),
		   rtps:add_participant(Domain_id, Guid_prefix),
		   fun() -> application:stop(rtps) end
	   end,
	   ?FORALL({Entity_key,
		    State_type,
		    Reliability_level}, {rtps:entity_key(),
					 oneof([stateless, stateful]),
					 oneof([best_effort, reliable])},
		   begin
		       Opts = [{state_type, State_type}, {reliability_level, Reliability_level}],
		       rtps:add_writer(Domain_id, Guid_prefix, Entity_key, Opts),
		       Writer_pid = rtps:whereis_writer(Domain_id, Guid_prefix, Entity_key),
		       true = is_pid(Writer_pid),
		       rtps:del_writer(Domain_id, Guid_prefix, Entity_key),
		       undefined =:= rtps:whereis_writer(Domain_id, Guid_prefix, Entity_key)
		   end)
	).

prop_add_reader() ->
    Domain_id = 0,
    Guid_prefix = <<1:96>>,
    ?SETUP(fun() -> 
		   application:start(rtps),
		   rtps:add_domain(Domain_id),
		   rtps:add_participant(Domain_id, Guid_prefix),
		   fun() -> application:stop(rtps) end
	   end,
	   ?FORALL({Entity_key,
	   	    State_type,
	   	    Reliability_level}, ?SUCHTHAT({_K, S, R},
	   					  {rtps:entity_key(),
	   					   oneof([stateless, stateful]),
	   					   oneof([best_effort, reliable])},
	   					  not(S =:= stateless andalso R =:= reliable)),
		   %%collect({State_type, Reliability_level},
		   begin
		       Opts = [{state_type, State_type}, {reliability_level, Reliability_level}],
		       case rtps:add_reader(Domain_id, Guid_prefix, Entity_key, Opts) of
			   {ok, _Pid} ->
			       true;
			   {error, {already_started, _Pid}} ->
			       true;
			   _ ->
			       false
		       end
		   end)%)
	  ).

prop_del_reader() ->
    Domain_id = 0,
    Guid_prefix = <<1:96>>,
    ?SETUP(fun() -> 
		   application:start(rtps),
		   rtps:add_domain(Domain_id),
		   rtps:add_participant(Domain_id, Guid_prefix),
		   fun() -> application:stop(rtps) end
	   end,
	   ?FORALL({Entity_key,
		    State_type,
		    Reliability_level}, ?SUCHTHAT({_K, S, R},
						  {rtps:entity_key(),
						   oneof([stateless, stateful]),
						   oneof([best_effort, reliable])},
						  not(S =:= stateless andalso R =:= reliable)),
		   begin
		       Opts = [{state_type, State_type}, {reliability_level, Reliability_level}],
		       rtps:add_reader(Domain_id, Guid_prefix, Entity_key, Opts),
		       Reader_pid = rtps:whereis_reader(Domain_id, Guid_prefix, Entity_key),
		       true = is_pid(Reader_pid),
		       rtps:del_reader(Domain_id, Guid_prefix, Entity_key),
		       undefined =:= rtps:whereis_reader(Domain_id, Guid_prefix, Entity_key)
		   end)
	).

%% In the following tests, changes are created individually and added
%% and removed from the history cache in the most basic manner
%% possible, which is correct but hopelessly inefficient.

prop_new_change() ->
    Domain_id = 0,
    Guid_prefix = <<1:96>>,
    Entity_key = <<1:24>>,
    State_type = stateless,
    Reliability_level = best_effort,
    Opts = [{state_type, State_type}, {reliability_level, Reliability_level}],
    ?SETUP(fun() -> 
		   application:start(rtps),
		   rtps:add_domain(Domain_id),
		   rtps:add_participant(Domain_id, Guid_prefix),
		   rtps:add_writer(Domain_id, Guid_prefix, Entity_key, Opts),
		   fun() -> application:stop(rtps) end
	   end,
	   ?FORALL({Kind, Handle, Data_value}, {rtps_history_cache:change_kind(),
						rtps_history_cache:instance_handle(),
						rtps_history_cache:data_value()},
		   begin
		       Writer_pid = rtps:whereis_writer(Domain_id, Guid_prefix, Entity_key),
		       case rtps_writer:new_change(Writer_pid, Kind, Data_value, Handle) of
			   {ok, #cache_change{kind = Kind, instance_handle = Handle, data_value = Data_value}} ->
			       true;
			   _ ->
			       false
		       end
		   end)
	  ).

prop_add_to_history_cache() ->
    Domain_id = 0,
    Guid_prefix = <<1:96>>,
    Entity_key = <<1:24>>,
    State_type = stateless,
    Reliability_level = best_effort,
    Opts = [{state_type, State_type}, {reliability_level, Reliability_level}],
    ?SETUP(fun() -> 
		   application:start(rtps),
		   rtps:add_domain(Domain_id),
		   rtps:add_participant(Domain_id, Guid_prefix),
		   rtps:add_writer(Domain_id, Guid_prefix, Entity_key, Opts),
		   fun() -> application:stop(rtps) end
	   end,
	   ?FORALL({Kind, Handle, Data_value}, {rtps_history_cache:change_kind(),
						rtps_history_cache:instance_handle(),
						rtps_history_cache:data_value()},
		   begin
		       Writer_pid = rtps:whereis_writer(Domain_id, Guid_prefix, Entity_key),
		       {ok, Change} = rtps_writer:new_change(Writer_pid, Kind, Data_value, Handle),
		       ok =:= rtps_writer:add_change(Writer_pid, Change)
		   end)
	  ).

prop_remove_from_history_cache() ->
    Domain_id = 0,
    Guid_prefix = <<1:96>>,
    Entity_key = <<1:24>>,
    State_type = stateless,
    Reliability_level = best_effort,
    Opts = [{state_type, State_type}, {reliability_level, Reliability_level}],
    ?SETUP(fun() -> 
		   application:start(rtps),
		   rtps:add_domain(Domain_id),
		   rtps:add_participant(Domain_id, Guid_prefix),
		   rtps:add_writer(Domain_id, Guid_prefix, Entity_key, Opts),
		   fun() -> application:stop(rtps) end
	   end,
	   ?FORALL({Kind, Handle, Data_value}, {rtps_history_cache:change_kind(),
						rtps_history_cache:instance_handle(),
						rtps_history_cache:data_value()},
		   begin
		       Writer_pid = rtps:whereis_writer(Domain_id, Guid_prefix, Entity_key),
		       {ok, Change} = rtps_writer:new_change(Writer_pid, Kind, Data_value, Handle),
		       ok = rtps_writer:add_change(Writer_pid, Change),
		       ok =:= rtps_writer:remove_change(Writer_pid, Change)
		   end)
	  ).

%%%%%%%%%%%%%%%
%%% Helpers %%%
%%%%%%%%%%%%%%%
%% boolean(_) -> true.

%%%%%%%%%%%%%%%%%%
%%% Generators %%%
%%%%%%%%%%%%%%%%%%
%% mytype() -> term().


items() ->
    ?SIZED(Size, [item(Id) || Id <- lists:seq(1, Size)]).
%%    ?LET(N, pos_integer(), [item(Id) || Id <- lists:seq(1, N)]).

item(Id) ->
    ?LET(Value, term(), {Id, Value}).

